\begin{tabbing}
($\backslash$p\=.let y = get\_var\_arg `n` p \+
\\[0ex]in let r = get\_term\_arg `f` p 
\\[0ex]in 
\\[0ex]((((((DTerm (
\-\\[0ex]m\=k\_apply\_term r (mvt y)) ({-}1)) \+
\\[0ex]CollapseTHENM (((DTerm (mvt y) ({-}1)) 
\\[0ex]CollapseTHENA (
\-\\[0ex]D\=eclaration))$\cdot$))$\cdot$) \+
\\[0ex]CollapseTHENM (D ({-}1)))$\cdot$) 
\\[0ex]CollapseTHENM (Hypothesis))$\cdot$ p)
\-
\end{tabbing}